0 Prolog
↳1 PrologToPiTRSProof (⇒, 44 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 1 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 32 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
PERM_IN_GA(X, .(X0, Y)) → U3_GA(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
PERM_IN_GA(X, .(X0, Y)) → APP1_IN_AAG(X1, .(X0, X2), X)
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → U1_AAG(X0, X, Y, Z, app1_in_aag(X, Y, Z))
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → APP1_IN_AAG(X, Y, Z)
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_GA(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → APP2_IN_GGA(X1, X2, Z)
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → U2_GGA(X0, X, Y, Z, app2_in_gga(X, Y, Z))
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → APP2_IN_GGA(X, Y, Z)
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_GA(X, X0, Y, perm_in_ga(Z, Y))
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → PERM_IN_GA(Z, Y)
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
PERM_IN_GA(X, .(X0, Y)) → U3_GA(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
PERM_IN_GA(X, .(X0, Y)) → APP1_IN_AAG(X1, .(X0, X2), X)
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → U1_AAG(X0, X, Y, Z, app1_in_aag(X, Y, Z))
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → APP1_IN_AAG(X, Y, Z)
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_GA(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → APP2_IN_GGA(X1, X2, Z)
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → U2_GGA(X0, X, Y, Z, app2_in_gga(X, Y, Z))
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → APP2_IN_GGA(X, Y, Z)
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_GA(X, X0, Y, perm_in_ga(Z, Y))
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → PERM_IN_GA(Z, Y)
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → APP2_IN_GGA(X, Y, Z)
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
APP2_IN_GGA(.(X0, X), Y, .(X0, Z)) → APP2_IN_GGA(X, Y, Z)
APP2_IN_GGA(.(X), Y) → APP2_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → APP1_IN_AAG(X, Y, Z)
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
APP1_IN_AAG(.(X0, X), Y, .(X0, Z)) → APP1_IN_AAG(X, Y, Z)
APP1_IN_AAG(.(Z)) → APP1_IN_AAG(Z)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_GA(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → PERM_IN_GA(Z, Y)
PERM_IN_GA(X, .(X0, Y)) → U3_GA(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
perm_in_ga(X, .(X0, Y)) → U3_ga(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_ga(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_ga(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U4_ga(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → U5_ga(X, X0, Y, perm_in_ga(Z, Y))
perm_in_ga([], []) → perm_out_ga([], [])
U5_ga(X, X0, Y, perm_out_ga(Z, Y)) → perm_out_ga(X, .(X0, Y))
U3_GA(X, X0, Y, app1_out_aag(X1, .(X0, X2), X)) → U4_GA(X, X0, Y, X1, X2, app2_in_gga(X1, X2, Z))
U4_GA(X, X0, Y, X1, X2, app2_out_gga(X1, X2, Z)) → PERM_IN_GA(Z, Y)
PERM_IN_GA(X, .(X0, Y)) → U3_GA(X, X0, Y, app1_in_aag(X1, .(X0, X2), X))
app2_in_gga(.(X0, X), Y, .(X0, Z)) → U2_gga(X0, X, Y, Z, app2_in_gga(X, Y, Z))
app2_in_gga([], Y, Y) → app2_out_gga([], Y, Y)
app1_in_aag(.(X0, X), Y, .(X0, Z)) → U1_aag(X0, X, Y, Z, app1_in_aag(X, Y, Z))
app1_in_aag([], Y, Y) → app1_out_aag([], Y, Y)
U2_gga(X0, X, Y, Z, app2_out_gga(X, Y, Z)) → app2_out_gga(.(X0, X), Y, .(X0, Z))
U1_aag(X0, X, Y, Z, app1_out_aag(X, Y, Z)) → app1_out_aag(.(X0, X), Y, .(X0, Z))
U3_GA(app1_out_aag(X1, .(X2))) → U4_GA(app2_in_gga(X1, X2))
U4_GA(app2_out_gga(Z)) → PERM_IN_GA(Z)
PERM_IN_GA(X) → U3_GA(app1_in_aag(X))
app2_in_gga(.(X), Y) → U2_gga(app2_in_gga(X, Y))
app2_in_gga([], Y) → app2_out_gga(Y)
app1_in_aag(.(Z)) → U1_aag(app1_in_aag(Z))
app1_in_aag(Y) → app1_out_aag([], Y)
U2_gga(app2_out_gga(Z)) → app2_out_gga(.(Z))
U1_aag(app1_out_aag(X, Y)) → app1_out_aag(.(X), Y)
app2_in_gga(x0, x1)
app1_in_aag(x0)
U2_gga(x0)
U1_aag(x0)
U3_GA(app1_out_aag(X1, .(X2))) → U4_GA(app2_in_gga(X1, X2))
U4_GA(app2_out_gga(Z)) → PERM_IN_GA(Z)
PERM_IN_GA(X) → U3_GA(app1_in_aag(X))
app2_in_gga(.(X), Y) → U2_gga(app2_in_gga(X, Y))
app2_in_gga([], Y) → app2_out_gga(Y)
app1_in_aag(.(Z)) → U1_aag(app1_in_aag(Z))
app1_in_aag(Y) → app1_out_aag([], Y)
U2_gga(app2_out_gga(Z)) → app2_out_gga(.(Z))
U1_aag(app1_out_aag(X, Y)) → app1_out_aag(.(X), Y)
U3GA1 > app1inaag1 > .1 > app2ingga2 > PERMINGA1 > U2gga1 > U1aag1 > U4GA1 > app1outaag2 > app2outgga1 > []
[]=2
._1=3
U2_gga_1=3
app2_out_gga_1=7
app1_in_aag_1=4
U1_aag_1=3
U3_GA_1=2
U4_GA_1=1
PERM_IN_GA_1=7
app2_in_gga_2=5
app1_out_aag_2=1
app2_in_gga(x0, x1)
app1_in_aag(x0)
U2_gga(x0)
U1_aag(x0)